In the Very Large-Scale Integration (VLSI) design industry, there are known procedures for detecting and rectifying logical defects in the design of processors, VLSI components, and various logical systems. Some formal verification methods are based on symbolic model checking, which is often limited with respect to the size of verifiable designs. In symbolic model checking, the concrete design is abstracted into a simpler design that has a smaller state space. The abstract design is typically an over-simplification of the concrete design, such that the abstract design often allows behaviors that are not allowed in the concrete design. This results in false negatives, as well as spurious counter-examples. In addition, present symbolic model checkers usually provide oily a single counter-example as the output of a failing verification. Furthermore, present symbolic model checkers cannot provide all the counter-examples of a given length as the output of a failing verification.
Other known methods of formal verification are based on Symbolic Trajectory Evaluation (STE) and symbolic simulation. In an STE model checker, counter-example information may be obtained from a failed run: the counter-example may be either symbolic, representing substantially all traces for which a property failed; or it may be a scalar representing only one trace for which the property failed. An STE model checker may also be designed to symbolically represent only a portion of the traces by constraining some of the values during the simulation. However, an STE model checker has limitations, for example: it may handle only a restricted class of properties; it may not handle arbitrary temporal properties; and it may not use some logical operators, e.g., disjunction.
There is no prior art method or apparatus to extract information on effectively all counter-examples of a given length on a symbolic model checking based run. Additionally, there is a need for solutions to produce various groups of counter-examples, e.g., counter-examples that may be used to debug and refine failures or to improve current abstractions.